(* [div] computes the integer division of two integers. *)
deferred val div : (int * int) -> int
where (forall (x, y). pre (div) (x, y) <=> not (y = 0))
 and (forall (x, y, z). post (div) (x, y) (z) <=> z = x / y)
